$\forall$$T$:Type, ${\it dT}$:EqDecider($T$), $L$:($T$ List), $x$, $y$:$T$.
\\[0ex]($x$ $\in$ $L$) $\Rightarrow$ ($y$ $\in$ $L$) $\Rightarrow$ (index($L$;$x$) $\leq$ index($L$;$y$)) $\Rightarrow$ ($x$ before $y$ $\in$ $L$ $\vee$ ($x$ = $y$))